\begin{tabbing}
$e$.$P$($e$) $\rightarrow$op$\rightarrow$ ${\it e'}$.$Q$(${\it e'}$) with $R$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=$f$:\{$e$:E$\mid$ $P$($e$)\} $\rightarrow$\{$e$:E$\mid$ $Q$($e$)\} \+
\\[0ex](($e$.$P$($e$) $\rightarrow$$a$.$f$($a$)$\rightarrow$ ${\it e'}$.$Q$(${\it e'}$)) with $R$ \& $e$.$f$($e$) is c$<$ preserving on $e$.$P$($e$))
\-
\end{tabbing}